es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p,q:({e:es-E(es)| 
es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p,q:({loc(e)
es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p,q:({=
es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p,q:({loc(e1)
es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p,q:({ Id} 
es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p,q:({e:es-E(es)| 
es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p,q:({loc(e)
es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p,q:({=
es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p,q:({loc(e1)
es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p,q:({ Id} 
es:event_system{i:l}, e1:es-E(es), e2:{e:es-E(es)| loc(e) = loc(e1)  Id} , p,q:(prop{i:l}).
[e1;e2]~([a,b].p(a,b))*[a,b].q(a,b)  prop{i:l} 

latex

Definitions	t  T, A c B, , x:A. B(x), A  B, P  Q, lelt(i; j; k), P  Q, False, A, int_seg(i; j), es-pred(es; e), es-E(es), Id, loc(e), prop{i:l}, x(s1,s2), es-locl(es; e; e'), es-le(es; e; e'), x:A. B(x), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), event_system{i:l}, P  Q, b, x. t(x), P  Q, P  Q, t.1, True, T
Lemmas	squash wf, true wf, int seg properties, nat plus properties, es-le-loc, es-loc-pred, or functionality wrt iff, all functionality wrt iff, es-locl-iff, event system wf, nat plus wf, es-le wf, es-locl wf, es-E wf, Id wf, es-loc wf, int seg wf, es-pred wf, le wf